------------- MODULE ralR1 -------------

EXTENDS Naturals, Sequences, TLC

CONSTANT L, \* décomposition binaire maximale de l'ensemble
         D  \* type des �l�ments

CHOIX == { "Insert", "Remove", "Put", "Get", "Occurrence", "Cardinal" }

Power2[i\in Nat] ==
 IF (i = 0) THEN 1 ELSE 2 * Power2[i - 1]

ELT == INSTANCE power2liste WITH P <- L, D <- D

\* Sequence avec le poids le plus faible en tete.
ETAT == [ 1..L -> ELT!ETAT ]

Inv(etat) ==
 /\ etat \in ETAT

Zero == << >>

\*---------------------------------------------------------------

\* Insérer un élément en tête de la liste (opération pile)
Insert[d \in ELT!ETAT, ss \in Seq(ELT!ETAT)] ==
 CASE (ss = Zero)           -> << ELT!Unit(d) >>
   [] (Head(ss) = ELT!Vide) -> LET hd == ELT!Unit(d) IN 
							   ELT!Join(hd, Tail(ss))
   [] OTHER                 -> LET hd == ELT!Join(d, Head(ss)) IN 
							   LET ins_succ == Insert[hd, Tail(ss)] IN
							   ELT!Join(<< ELT!Vide >>, ins_succ)

\*---------------------------------------------------------------

\* Retirer l'élément en tête de la liste (opération pile)
Remove[ss \in Seq(ELT!ETAT)] ==
 CASE (Len(ss) = 1)			-> [ result |-> << ELT!Vide >>,
                                 borrow |-> Head(ss) ]
   [] (Head(ss) = ELT!Vide) -> LET dec_succ == Remove[Tail(ss)] IN
                               LET split == ELT!Split(dec_succ.borrow) IN
                               [ result |-> ELT!Join(<< split[1] >>, dec_succ.result),
                                 borrow |-> split[2] ]
   [] OTHER                 -> [ result |-> ELT!Join(<< ELT!Vide >>, Tail(ss)),
                                 borrow |-> Head(ss) ]

\*---------------------------------------------------------------

\* updateCase fonction recursive appelée par updateR
updateCase[i \in Nat, d\in D, ss \in ELT!ETAT] == [ss EXCEPT ![i] = d] 

\* updateR fonction récursives appelée par Put
updateR[taille \in Nat, i \in Nat, d \in D, ss \in Seq(ELT!ETAT)] ==
 CASE ss = ELT!Vide			 -> ss
 	[] (Head(ss) = ELT!Vide) -> ELT!Join(ELT!Unit(Head(ss)), updateR[2*taille, i, d, Tail(ss)])
	[] OTHER                 -> \* Head(ss) non vide
 				CASE (i <= taille)	-> ELT!Join(ELT!Unit(updateCase[i, d, Head(ss)]), Tail(ss))
 				  [] OTHER			-> ELT!Join(ELT!Unit(Head(ss)), updateR[2*taille, (i - taille), d, Tail(ss)])
 				  
\* Modifier le contenu de la case i (opération tableau)                                  
Put[i \in Nat, d \in D, ss \in Seq(ELT!ETAT)] == updateR[1, i, d, ss]  

\*---------------------------------------------------------------

\* lookupCase fonction recursive appelée par lookupR
lookupCase[i \in Nat, ss \in ELT!ETAT] == ss[i] 

\* lookupR fonction recursive appelée par Get
lookupR[taille \in Nat, i \in Nat, ss \in Seq(ELT!ETAT)] == 
 CASE (ss = ELT!Vide)		-> ELT!Vide
   [] (Head(ss) = ELT!Vide) -> lookupR[2*taille, i, Tail(ss)]
   [] OTHER                 -> \* Head(ss) non vide
 				CASE (i <= taille)	-> lookupCase[i, Head(ss)]
 				  [] OTHER			-> lookupR[2*taille, (i - taille), Tail(ss)]

\* Accéder à la case i (opération tableau)                                  
Get[i \in Nat, ss \in Seq(ELT!ETAT)] == lookupR[1, i, ss]                   

\*---------------------------------------------------------------

\* Occurrence 				  
Occurrence[ss \in Seq(ELT!ETAT), d \in D] ==
	LET Aux[s \in Seq'ELT!ETAT, cpt \in Nat] ==
	CASE (s = << >>)		-> cpt
	[] OTHER				-> CASE (Head(s) = ELT!VIDE)		-> Aux[Tail(s), elt, cpt*2]
							   [] OTHER							-> Aux[Tail(s), ELT!Occurrence(Head(s), d)]
	IN Aux[ss, 0]

\*---------------------------------------------------------------

Cardinal[ss \in Seq(ELT!ETAT)] ==
	LET Aux[s \in Seq(ELT!ETAT), elt \in Nat, cpt \in Nat] ==
	CASE (s = << >>)		-> elt
	[] OTHER				-> CASE (Head(s) = ELT!VIDE)	-> Aux[Tail(s), elt, cpt*2]
							   [] OTHER						-> Aux[Tail(s), elt+cpt, cpt*2]
	IN Aux[ss, 0, 1]

\*---------------------------------------------------------------


BitToInteger[b\in ELT!ETAT] ==
 IF (b = ELT!Vide) THEN 0 ELSE 1

BinaryToInteger[s \in Seq(ELT!ETAT)] ==
 IF (s = Zero) THEN 0 ELSE
 BitToInteger[Head(s)] + 2*BinaryToInteger[Tail(s)]

-------------------------------------------

\* �tat initial
Init(etat) ==
 /\ etat = [ i \in 1..L |-> ELT!Vide ]

\* incr�menter
Pre_Insert(param, etat) ==
 /\ param \in D
 /\ \E i \in 1..L : etat[i] = ELT!Vide

Act_Insert(param, etat, etat_p, result) ==
 LET inc == Insert[ELT!Unit(param), etat] IN
 /\ etat_p = inc
 /\ result = "__NO_DATA"

\* d�cr�menter
Pre_Remove(param, etat) ==
 /\ param = "__NO_DATA"
 /\ \E i \in 1..L : etat[i] # ELT!Vide

Act_Remove(param, etat, etat_p, result) ==
 LET dec == Remove[etat] IN
 /\ etat_p = dec.result
 /\ ELT!Pick(dec.borrow, result)

\* Put
Pre_Put(param, etat) ==
 /\ param \in [ indice : 1..Cardinal[etat], valeur : D ]
 /\ LET get == Get[param.indice, etat] IN << get >> # ELT!Vide

Act_Put(param, etat, etat_p, result) ==
 LET inc == Put[param.indice, param.valeur, etat] IN
 /\ etat_p = inc
 /\ result = "__NO_DATA"

\* Get
Pre_Get(param, etat) ==
 /\ param \in 1..Cardinal(etat)
 
Act_Get(param, etat, etat_p, result) ==
LET dec == Get[param, etat] IN
 /\ etat_p = etat
 /\ result = dec

\* cardinal
Pre_Cardinal(param, etat) ==
 /\ param = "__NO_DATA"

Act_Cardinal(param, etat, etat_p, result) ==
 /\ etat_p = etat
 /\ result = Cardinal[etat]
 
 \* occurrence
Pre_Occurrence(param, etat) ==
 /\ param \in D

Act_Occurrence(param, etat, etat_p, result) ==
LET oc == Occurrence[param, etat] IN
 /\ etat_p = etat
 /\ result = oc
                                  
-------------------------------------------

ContratClient(choix, param, etat) ==
 \/ (choix = "Insert"     /\ Pre_Insert(param, etat))
 \/ (choix = "Remove"     /\ Pre_Remove(param, etat))
 \/ (choix = "Put"        /\ Pre_Put(param, etat))
 \/ (choix = "Get"        /\ Pre_Get(param, etat))
 \/ (choix = "Occurrence" /\ Pre_Occurrence(param, etat))
 \/ (choix = "Cardinal"   /\ Pre_Cardinal(param, etat))

ContratModule(choix, param, etat, etat_prime, result) ==
 /\ (choix = "Insert"     => (Pre_Insert(param, etat)     => Act_Insert(param, etat, etat_prime, result)))
 /\ (choix = "Remove"     => (Pre_Remove(param, etat)     => Act_Remove(param, etat, etat_prime, result)))
 /\ (choix = "Put"        => (Pre_Put(param, etat)        => Act_Put(param, etat, etat_prime, result)))
 /\ (choix = "Get"        => (Pre_Get(param, etat)        => Act_Get(param, etat, etat_prime, result)))
 /\ (choix = "Occurrence" => (Pre_Occurrence(param, etat) => Act_Occurrence(param, etat, etat_prime, result)))
 /\ (choix = "Cardinal"   => (Pre_Cardinal(param, etat)   => Act_Cardinal(param, etat, etat_prime, result)))

===========================================
